COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	situat[e82,jmc]		situation calculus and axioms
C00014 00003	The frame problem
C00020 ENDMK
C⊗;
situat[e82,jmc]		situation calculus and axioms

NOTES ON THE SITUATION CALCULUS


	The object of these notes is to axiomatize as much common sense
knowledge as possible using the situation calculus.
We will use circumscription to simplify the axioms as much as
possible.

	How much common sense can be axiomatized in the situation calculus
is limited for several reasons:

	1. The situation calculus cannot deal with concurrent events
reasonably.  Can this actually be proved?

	2. The formulations we shall use don't properly allow
intensional use of the formulas, e.g. we can't properly refer
to beliefs.

	3. We haven't a good way of relating approximate theories
to better and worse approximations.

	Nevertheless, the situation calculus has proved useful, and
circumcription makes it even more useful.


Situations

	A situation is regarded as a snapshot of the world at an
instant of time.  We don't fully describe situations, but we give
facts about situations.  A typical fact is

	on(A,B,s),

asserting that block A is on block B in situation s.
We also have functions like  height(x,s)  giving the height of
block  x  in siutuation  s.


Change

	Events occur in situations and give rise to new situations.
Thus we may write

(a1)	s' = move(x,y,s)

to assert that the situation  s'  results from moving block  x onto
block  y  in situation  s.


Reification

	To reify (from Latin  "re"  meaning "thing") is to regard an
abstract entity as a thing.  In first order logic, this means making
it an element of the domain, or in sorted logic, a member of some sort.
If we want to quantify over some class of entities, they must be
elments of the domain.  This is best understood by examples.  We
will usually write

	s' = result(e,s)

meaning that  s'  is the situation that results when event  e  occurs
in the situation  s.  We can regard  Move(x,y)  as a possible value
of  e  and write

(a2)	s' = result(Move(x,y),s).

	(a2) will be used in preference to  (a1) when we want to
quantify over events.  Thus we may have a general rule about
events

	∀e. ...etc.

and we can get a result about moving  x  onto  y  by substituting
Move(x,y)  for  e  in the general rule.  Often we will use both
notations interchangably and can write

	∀x y s. move(x,y,s) = result(Move(x,y),s).

The  result  notation is longer, and we will see that no matter how
much reification has been done, it can always be elaborated further,
so we do only as much reification as we have actual use for.  That
is we introduce a new class of objects only if formalizing the
particular domain of common sense requires general statements about
this class of objects.

	Another example of reification involves writing

	holds(On(x,y),s)

instead of

	on(x,y,s).

This allows quantifying over assertions that may or may not hold in
a situation.  We use the word  "fluent"  for entities like On(x,y) that have values
in situations.


The blocks world

	We begin by considering the action of moving one block onto
another.  The simplest way to assert that one block will be on the
other after this action is

	∀x y s.on(x,y,move(x,y,s)).

	However, there are usually considered to be preconditions
for the successful performance of this action.  The old (before
circumscription) way was to take some of them into account by
writing

	∀x y s.clear(x,s) ∧ clear(y,s) ⊃ on(x,y,move(x,y,s)),

where we define the condition  clear(x,s)  by

	∀x s.clear(x,s) ≡ ∀z.¬on(z,x,s).

When we wanted to use rules that quantify over events, we wrote

	∀x y s. clear(x,s) ∧ clear(y,s) ⊃ on(x,y,result(Move(x,y),s)).

	It may sometimes be advantageous to summarize the conditions
for successful performance of moving the block into a condition
by writing

	∀x ys.succeeds(Move(x,y),s) ⊃ on(x,y,result(Move(x,y),s)).

We then write

	∀x y s.clear(x,s) ∧ clear(y,s) ∧ ¬prevented(Move(x,y),s)
⊃ succeeds(Move(x,y),s)


Use of circumscription

	Circumscription is a rule of conjecture that can be used
to draw conclusions based on simplest models of the facts "that are
taken into account".  It is described in (McCarthy 1980).  It is
a non-monotonic mode of reasoning in that taking more facts into
account may cause some previous conclusions not to be inferred.

	In the present case, we suppose that we take into account the
general facts about moving listed above together with the facts
available about the particular situation  s.

	If we now circumscribe both  succeeds  and  prevented  we will
require positive knowledge that  x  and  y  are clear before we
conclude that the action will have its standard effect, but all other
things that might go wrong require positive evidence.  Thus we may
add

	∀x y s.tooheavy(x) ⊃ prevented(Move(x,y),s).

Now circumscribing  succeeds,  prevented,  and  tooheavy has the desired
effect of requiring positive evidence that  x  and  y  are clear but
assuming that  x  isn't too heavy unless that follows from information
taken into account.

	Now let us consider methods of controlling what circumscriptions
are done.  Suppose we introduce a modal operator called  UNLIKELY  and
the assertions

	∀x y s.UNLIKELY succeeds(Move(x,y),s),

	∀x s. UNLIKELY clear(x,s)

	∀x y s.UNLIKELY prevented(Move(x,y),s),

and

	∀x. UNLIKELY tooheavy(x).

This is to be taken as a guide to the reasoning program to circumscribe
succeeds(Move(x,y),s),  clear(x,s),  prevented(Move(x,y),s)  and
tooheavy(x).
The circumscription will be performed using as an axiom the total collection
of facts that are taken into account.  The axioms so far assure that
we will have to show that  x  and  y  are clear, but  x  will not be assumed
to be too heavy.  However, if there is information asserting that  x
is too heavy, it will be used to inhibit deducing that the blocks can
be moved.

	UNLIKELY  has to be treated as a modal operator, since
the truth of  UNLIKELY succeeds(Move(x,y),s)  is not just a function
of the value (truth value) of  succeeds(Move(x,y),s).  In order to
bring the theory back into first order logic we have to reify all
expressions that may be circumscribed.  We define

	holds(Succeeds(Move(x,y)),s) ≡ succeeds(Move(x,y),s)

and can now write

	∀x y s.UNLIKELY Succeeds(Move(x,y),s), etc.

What gets circumscribed now is

	holds(Succeeds(Move(x,y)),s).

UNLIKELY  is now just an ordinary predicate but one which is given a
special role by the reasoning program.
We emphasize that the reasoning is still non-monotonic, because the
circumscriptions are done after it has been decided what facts to take
into account, and the conclusions are a non-monotonic function of
this collection of facts.

	In principle, the predicate  UNLIKELY  can
used to form more complex expressions.  However, we haven't studied
what these expressions mean.  Conjuctions offer no problem and give
rise to simultaneous circumscriptions.  However, disjunction and
even negation are problematical.  To say

	¬UNLIKELY tooheavy x

seems only to suggest that a circumscription not be done.  Iterating
UNLIKELY  is probably worthwhile.  It means that circumscription may
be used in deciding what circumscriptions to do.  Presumably there
will be addtional problems involving quantifiers.  Moreover, with
quantifiers, the possibility arises of constructing self-referent
expressions.  Probably the opportunities for
self-reference will attract logicians,
philosophers and Doug Hofstadter as honey
attracts flies but will have limited application to formalizing
common sense.
The frame problem
Overdoing reification

Note on concurrent events:

	If our result conclusion is ordinarily that a fluent held
at some time in the past, we may be able to draw many concurrent
event conclusions without having to assert that two fluents
on different causal lines were ever true at the same time.  Thus
the tense is "will have happened".

Problems in formalizing common sense

1. Design and construction and the partially built tower, etc.


	3. Note on circumscription versus non-monotonic logic.

We do "The meeting will be held on Wednesday unless there is a reason
to hold it on some other day" as 

	 UNLIKELY not w

where  w  is the proposition that the meeting will be on Wednesday.
Note that circumscription has the opposite sign from the
McDermott-Doyle

	Mp ⊃ p.

However, circumscription has the heuristically convenient sign whenever
quantification is involved, because we often want to say that a
predicate applies to as few arguments as possible and never to say that
it applies to as many arguments as possible.

Perhaps we should change UNLIKELY to MINIMIZE or even CIRCUMSCRIBE.